k:Knd, L:Id List. k affects only members of L  MsgA 

latex

Definitions	Id, t  T, Knd, type List, x.A(x), x. t(x), x:A. B(x), , IdLnk, x : v, x:AB(x), Void, Type, Top, x:AB(x), State(ds), Prop, mk-ma, k affects only members of L, MsgA
Lemmas	mk-ma wf, ma-state wf, top wf, fpf-single wf, IdLnk wf, fpf-empty wf, Knd wf, Id wf